{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "28f1bcf3",
   "metadata": {},
   "outputs": [],
   "source": [
    "import pandas as pd\n",
    "import numpy as np"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "6b4114aa",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "6   CC85(a)       agree0      9      18     342.0        4.93\n",
       "0   CC85(a)  termination      9      16     171.5        3.36\n",
       "7   CC85(a)       valid0      9      18      42.0        0.50\n",
       "8   CC85(b)       agree0     10      17       6.0        0.25\n",
       "1   CC85(b)  termination     10      15       8.0        0.40\n",
       "9   CC85(b)       valid0     10      17       2.0        0.20\n",
       "10    FMR05       agree0     10      11       6.0        0.23\n",
       "2     FMR05  termination     10       6       2.0        0.41\n",
       "11    FMR05       valid0     10      11       2.0        0.21\n",
       "12     KS16       agree0     11      23      18.0        0.75\n",
       "3      KS16  termination     11      28      15.0        1.02\n",
       "13     KS16       valid0     11      23       5.0        0.31\n",
       "14    MMR14       agree0     17      29   28916.2      298.90\n",
       "5     MMR14  termination     16      27       NaN         NaN\n",
       "15    MMR14       valid0     17      29    1442.2        8.74\n",
       "16  Rabin83       agree0     10      15       6.0        0.25\n",
       "4   Rabin83  termination     10       9       8.0        0.43\n",
       "17  Rabin83       valid0     10      15       2.0        0.20"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "data_file='./tech_ltl_10runs_simp.csv'\n",
    "df=pd.read_csv(data_file)\n",
    "df.sort_values(by=['Name','Formula'],inplace=True)\n",
    "df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "a7109e42",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "0   Rabin83       agree0     10      15       6.0        0.25\n",
       "1   Rabin83  termination     10       9       8.0        0.43\n",
       "2   Rabin83       valid0     10      15       2.0        0.20\n",
       "3   CC85(a)       agree0      9      18     342.0        4.93\n",
       "4   CC85(a)  termination      9      16     171.5        3.36\n",
       "5   CC85(a)       valid0      9      18      42.0        0.50\n",
       "6   CC85(b)       agree0     10      17       6.0        0.25\n",
       "7   CC85(b)  termination     10      15       8.0        0.40\n",
       "8   CC85(b)       valid0     10      17       2.0        0.20\n",
       "9     FMR05       agree0     10      11       6.0        0.23\n",
       "10    FMR05  termination     10       6       2.0        0.41\n",
       "11    FMR05       valid0     10      11       2.0        0.21\n",
       "12     KS16       agree0     11      23      18.0        0.75\n",
       "13     KS16  termination     11      28      15.0        1.02\n",
       "14     KS16       valid0     11      23       5.0        0.31\n",
       "15    MMR14       agree0     17      29   28916.2      298.90\n",
       "16    MMR14  termination     16      27       NaN         NaN\n",
       "17    MMR14       valid0     17      29    1442.2        8.74"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rabin83_rows = df[df['Name'] == 'Rabin83']\n",
    "df = pd.concat([rabin83_rows, df[df['Name'] != 'Rabin83']])\n",
    "df.reset_index(drop=True, inplace=True)\n",
    "df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "3d3d9a9d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "0   Rabin83       agree0     10      15       6.0        0.25\n",
       "1   Rabin83  termination     10       9       8.0        0.43\n",
       "2   Rabin83       valid0     10      15       2.0        0.20\n",
       "3   CC85(a)       agree0      9      18     342.0        4.93\n",
       "4   CC85(a)  termination      9      16     171.5        3.36\n",
       "5   CC85(a)       valid0      9      18      42.0        0.50\n",
       "6   CC85(b)       agree0     10      17       6.0        0.25\n",
       "7   CC85(b)  termination     10      15       8.0        0.40\n",
       "8   CC85(b)       valid0     10      17       2.0        0.20\n",
       "9     FMR05       agree0     10      11       6.0        0.23\n",
       "10    FMR05  termination     10       6       2.0        0.41\n",
       "11    FMR05       valid0     10      11       2.0        0.21\n",
       "12     KS16       agree0     11      23      18.0        0.75\n",
       "13     KS16  termination     11      28      15.0        1.02\n",
       "14     KS16       valid0     11      23       5.0        0.31\n",
       "15    MMR14       agree0     17      29   28916.2      298.90\n",
       "16    MMR14  termination     16      27       NaN         NaN\n",
       "17    MMR14       valid0     17      29    1442.2        8.74"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "14baea24",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "0   Rabin83       agree0     10      15       6.0        0.25\n",
       "1   Rabin83  termination     10       9       8.0        0.43\n",
       "2   Rabin83       valid0     10      15       2.0        0.20\n",
       "3   CC85(a)       agree0      9      18     342.0        4.93\n",
       "4   CC85(a)  termination      9      16     171.5        3.36\n",
       "5   CC85(a)       valid0      9      18      42.0        0.50\n",
       "6   CC85(b)       agree0     10      17       6.0        0.25\n",
       "7   CC85(b)  termination     10      15       8.0        0.40\n",
       "8   CC85(b)       valid0     10      17       2.0        0.20\n",
       "9     FMR05       agree0     10      11       6.0        0.23\n",
       "10    FMR05  termination     10       6       2.0        0.41\n",
       "11    FMR05       valid0     10      11       2.0        0.21\n",
       "12     KS16       agree0     11      23      18.0        0.75\n",
       "13     KS16  termination     11      28      15.0        1.02\n",
       "14     KS16       valid0     11      23       5.0        0.31\n",
       "15    MMR14       agree0     17      29   28916.2      298.90\n",
       "16    MMR14  termination     16      27       NaN         NaN\n",
       "17    MMR14       valid0     17      29    1442.2        8.74"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "11769c56",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "0   Rabin83  agree0     10      15       6.0        0.25\n",
       "3   CC85(a)  agree0      9      18     342.0        4.93\n",
       "6   CC85(b)  agree0     10      17       6.0        0.25\n",
       "9     FMR05  agree0     10      11       6.0        0.23\n",
       "12     KS16  agree0     11      23      18.0        0.75\n",
       "15    MMR14  agree0     17      29   28916.2      298.90"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "filtered_df = df[df['Formula'] == 'agree0']\n",
    "filtered_df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "e128107e",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "C:\\Users\\gaos_\\AppData\\Local\\Temp\\ipykernel_22364\\3430040888.py:3: SettingWithCopyWarning: \n",
      "A value is trying to be set on a copy of a slice from a DataFrame.\n",
      "Try using .loc[row_indexer,col_indexer] = value instead\n",
      "\n",
      "See the caveats in the documentation: https://pandas.pydata.org/pandas-docs/stable/user_guide/indexing.html#returning-a-view-versus-a-copy\n",
      "  filtered_df['nmilestones'] = nmilestones_data\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "      <th>nmilestones</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "      <td>0</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "      <td>3</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "      <td>0</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "      <td>0</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "      <td>1</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "      <td>6</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name Formula  nlocs  nrules  nschemas  elapsedsec  nmilestones\n",
       "0   Rabin83  agree0     10      15       6.0        0.25            0\n",
       "3   CC85(a)  agree0      9      18     342.0        4.93            3\n",
       "6   CC85(b)  agree0     10      17       6.0        0.25            0\n",
       "9     FMR05  agree0     10      11       6.0        0.23            0\n",
       "12     KS16  agree0     11      23      18.0        0.75            1\n",
       "15    MMR14  agree0     17      29   28916.2      298.90            6"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# 假设 filtered_df 是你筛选后的数据框\n",
    "nmilestones_data = [0, 3, 0, 0, 1, 6]\n",
    "filtered_df['nmilestones'] = nmilestones_data\n",
    "\n",
    "# 显示更新后的数据框\n",
    "filtered_df"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "ef30471d",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nmilestones</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>3</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>1</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>6</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name Formula  nlocs  nrules  nmilestones  nschemas  elapsedsec\n",
       "0   Rabin83  agree0     10      15            0       6.0        0.25\n",
       "3   CC85(a)  agree0      9      18            3     342.0        4.93\n",
       "6   CC85(b)  agree0     10      17            0       6.0        0.25\n",
       "9     FMR05  agree0     10      11            0       6.0        0.23\n",
       "12     KS16  agree0     11      23            1      18.0        0.75\n",
       "15    MMR14  agree0     17      29            6   28916.2      298.90"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# 假设 filtered_df 是你筛选后的数据框\n",
    "new_order = ['Name', 'Formula', 'nlocs', 'nrules', 'nmilestones', 'nschemas', 'elapsedsec']\n",
    "filtered_df = filtered_df[new_order]\n",
    "\n",
    "# 显示更新后的数据框\n",
    "filtered_df\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "c46ce2ef",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "2   Rabin83  valid0     10      15       2.0        0.20\n",
       "5   CC85(a)  valid0      9      18      42.0        0.50\n",
       "8   CC85(b)  valid0     10      17       2.0        0.20\n",
       "11    FMR05  valid0     10      11       2.0        0.21\n",
       "14     KS16  valid0     11      23       5.0        0.31\n",
       "17    MMR14  valid0     17      29    1442.2        8.74"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "validdf = df[df['Formula'] == 'valid0']\n",
    "validdf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "57f2cbb0",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "C:\\Users\\gaos_\\AppData\\Local\\Temp\\ipykernel_22364\\41869995.py:1: SettingWithCopyWarning: \n",
      "A value is trying to be set on a copy of a slice from a DataFrame.\n",
      "Try using .loc[row_indexer,col_indexer] = value instead\n",
      "\n",
      "See the caveats in the documentation: https://pandas.pydata.org/pandas-docs/stable/user_guide/indexing.html#returning-a-view-versus-a-copy\n",
      "  validdf['nmilestones']=nmilestones_data\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nmilestones</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>3</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>1</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>6</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name Formula  nlocs  nrules  nmilestones  nschemas  elapsedsec\n",
       "2   Rabin83  valid0     10      15            0       2.0        0.20\n",
       "5   CC85(a)  valid0      9      18            3      42.0        0.50\n",
       "8   CC85(b)  valid0     10      17            0       2.0        0.20\n",
       "11    FMR05  valid0     10      11            0       2.0        0.21\n",
       "14     KS16  valid0     11      23            1       5.0        0.31\n",
       "17    MMR14  valid0     17      29            6    1442.2        8.74"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "validdf['nmilestones']=nmilestones_data\n",
    "validdf=validdf[new_order]\n",
    "validdf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "8d88c93e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nschemas  elapsedsec\n",
       "1   Rabin83  termination     10       9       8.0        0.43\n",
       "4   CC85(a)  termination      9      16     171.5        3.36\n",
       "7   CC85(b)  termination     10      15       8.0        0.40\n",
       "10    FMR05  termination     10       6       2.0        0.41\n",
       "13     KS16  termination     11      28      15.0        1.02\n",
       "16    MMR14  termination     16      27       NaN         NaN"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "termindf= df[df['Formula'] == 'termination']\n",
    "termindf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "5e1c5fc5",
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "C:\\Users\\gaos_\\AppData\\Local\\Temp\\ipykernel_22364\\1466474300.py:1: SettingWithCopyWarning: \n",
      "A value is trying to be set on a copy of a slice from a DataFrame.\n",
      "Try using .loc[row_indexer,col_indexer] = value instead\n",
      "\n",
      "See the caveats in the documentation: https://pandas.pydata.org/pandas-docs/stable/user_guide/indexing.html#returning-a-view-versus-a-copy\n",
      "  termindf['nmilestones']=nmilestones_data\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nmilestones</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>0</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>3</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>1</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>6</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nmilestones  nschemas  elapsedsec\n",
       "1   Rabin83  termination     10       9            0       8.0        0.43\n",
       "4   CC85(a)  termination      9      16            3     171.5        3.36\n",
       "7   CC85(b)  termination     10      15            0       8.0        0.40\n",
       "10    FMR05  termination     10       6            0       2.0        0.41\n",
       "13     KS16  termination     11      28            1      15.0        1.02\n",
       "16    MMR14  termination     16      27            6       NaN         NaN"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "termindf['nmilestones']=nmilestones_data\n",
    "termindf=termindf[new_order]\n",
    "termindf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "6bf8321e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>Name</th>\n",
       "      <th>Formula</th>\n",
       "      <th>nlocs</th>\n",
       "      <th>nrules</th>\n",
       "      <th>nmilestones</th>\n",
       "      <th>nschemas</th>\n",
       "      <th>elapsedsec</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>3</td>\n",
       "      <td>342.0</td>\n",
       "      <td>4.93</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.25</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>agree0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>0</td>\n",
       "      <td>6.0</td>\n",
       "      <td>0.23</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>KS16</td>\n",
       "      <td>agree0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>1</td>\n",
       "      <td>18.0</td>\n",
       "      <td>0.75</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>5</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>agree0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>6</td>\n",
       "      <td>28916.2</td>\n",
       "      <td>298.90</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>6</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>7</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>9</td>\n",
       "      <td>18</td>\n",
       "      <td>3</td>\n",
       "      <td>42.0</td>\n",
       "      <td>0.50</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>8</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>17</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.20</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>9</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>valid0</td>\n",
       "      <td>10</td>\n",
       "      <td>11</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.21</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>10</th>\n",
       "      <td>KS16</td>\n",
       "      <td>valid0</td>\n",
       "      <td>11</td>\n",
       "      <td>23</td>\n",
       "      <td>1</td>\n",
       "      <td>5.0</td>\n",
       "      <td>0.31</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>11</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>valid0</td>\n",
       "      <td>17</td>\n",
       "      <td>29</td>\n",
       "      <td>6</td>\n",
       "      <td>1442.2</td>\n",
       "      <td>8.74</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>12</th>\n",
       "      <td>Rabin83</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>9</td>\n",
       "      <td>0</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.43</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>13</th>\n",
       "      <td>CC85(a)</td>\n",
       "      <td>termination</td>\n",
       "      <td>9</td>\n",
       "      <td>16</td>\n",
       "      <td>3</td>\n",
       "      <td>171.5</td>\n",
       "      <td>3.36</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>14</th>\n",
       "      <td>CC85(b)</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>15</td>\n",
       "      <td>0</td>\n",
       "      <td>8.0</td>\n",
       "      <td>0.40</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>15</th>\n",
       "      <td>FMR05</td>\n",
       "      <td>termination</td>\n",
       "      <td>10</td>\n",
       "      <td>6</td>\n",
       "      <td>0</td>\n",
       "      <td>2.0</td>\n",
       "      <td>0.41</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>16</th>\n",
       "      <td>KS16</td>\n",
       "      <td>termination</td>\n",
       "      <td>11</td>\n",
       "      <td>28</td>\n",
       "      <td>1</td>\n",
       "      <td>15.0</td>\n",
       "      <td>1.02</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>17</th>\n",
       "      <td>MMR14</td>\n",
       "      <td>termination</td>\n",
       "      <td>16</td>\n",
       "      <td>27</td>\n",
       "      <td>6</td>\n",
       "      <td>NaN</td>\n",
       "      <td>NaN</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "</div>"
      ],
      "text/plain": [
       "       Name      Formula  nlocs  nrules  nmilestones  nschemas  elapsedsec\n",
       "0   Rabin83       agree0     10      15            0       6.0        0.25\n",
       "1   CC85(a)       agree0      9      18            3     342.0        4.93\n",
       "2   CC85(b)       agree0     10      17            0       6.0        0.25\n",
       "3     FMR05       agree0     10      11            0       6.0        0.23\n",
       "4      KS16       agree0     11      23            1      18.0        0.75\n",
       "5     MMR14       agree0     17      29            6   28916.2      298.90\n",
       "6   Rabin83       valid0     10      15            0       2.0        0.20\n",
       "7   CC85(a)       valid0      9      18            3      42.0        0.50\n",
       "8   CC85(b)       valid0     10      17            0       2.0        0.20\n",
       "9     FMR05       valid0     10      11            0       2.0        0.21\n",
       "10     KS16       valid0     11      23            1       5.0        0.31\n",
       "11    MMR14       valid0     17      29            6    1442.2        8.74\n",
       "12  Rabin83  termination     10       9            0       8.0        0.43\n",
       "13  CC85(a)  termination      9      16            3     171.5        3.36\n",
       "14  CC85(b)  termination     10      15            0       8.0        0.40\n",
       "15    FMR05  termination     10       6            0       2.0        0.41\n",
       "16     KS16  termination     11      28            1      15.0        1.02\n",
       "17    MMR14  termination     16      27            6       NaN         NaN"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "combinedf=pd.concat([filtered_df,validdf,termindf],ignore_index=True)\n",
    "combinedf"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "62c08706",
   "metadata": {},
   "outputs": [],
   "source": [
    "saved_csv='./tech_ltl_10runs_final.csv'\n",
    "combinedf.to_csv(saved_csv, index=False)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "76c68c1f",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
